H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 206.952 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((isAlpha :: Char -> Bool) :: Char -> Bool)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((isAlpha :: Char -> Bool) :: Char -> Bool)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((isAlpha :: Char -> Bool) :: Char -> Bool)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(isAlpha :: Char -> Bool)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="isAlpha",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="isAlpha vx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="isUpper vx3 || isLower vx3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5 -> 49[label="",style="dashed", color="red", weight=0];
5[label="(vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || isLower vx3",fontsize=16,color="magenta"];5 -> 50[label="",style="dashed", color="magenta", weight=3];
5 -> 51[label="",style="dashed", color="magenta", weight=3];
5 -> 52[label="",style="dashed", color="magenta", weight=3];
5 -> 53[label="",style="dashed", color="magenta", weight=3];
5 -> 54[label="",style="dashed", color="magenta", weight=3];
5 -> 55[label="",style="dashed", color="magenta", weight=3];
5 -> 56[label="",style="dashed", color="magenta", weight=3];
50[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];51[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];52[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];53[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];54[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];55[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];56[label="vx3",fontsize=16,color="green",shape="box"];49[label="(vx30 >= Char (Succ vx31) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)) || isLower vx30",fontsize=16,color="black",shape="triangle"];49 -> 64[label="",style="solid", color="black", weight=3];
64[label="(compare vx30 (Char (Succ vx31)) /= LT && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)) || isLower vx30",fontsize=16,color="black",shape="box"];64 -> 65[label="",style="solid", color="black", weight=3];
65[label="(not (compare vx30 (Char (Succ vx31)) == LT) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)) || isLower vx30",fontsize=16,color="black",shape="box"];65 -> 66[label="",style="solid", color="black", weight=3];
66[label="(not (primCmpChar vx30 (Char (Succ vx31)) == LT) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)) || isLower vx30",fontsize=16,color="burlywood",shape="box"];2030[label="vx30/Char vx300",fontsize=10,color="white",style="solid",shape="box"];66 -> 2030[label="",style="solid", color="burlywood", weight=9];
2030 -> 67[label="",style="solid", color="burlywood", weight=3];
67[label="(not (primCmpChar (Char vx300) (Char (Succ vx31)) == LT) && Char vx300 <= Char (Succ vx32) || Char vx300 >= Char (Succ vx33) && Char vx300 <= Char (Succ vx34) || Char vx300 >= Char (Succ vx35) && Char vx300 <= Char (Succ vx36)) || isLower (Char vx300)",fontsize=16,color="black",shape="box"];67 -> 68[label="",style="solid", color="black", weight=3];
68[label="(not (primCmpNat vx300 (Succ vx31) == LT) && Char vx300 <= Char (Succ vx32) || Char vx300 >= Char (Succ vx33) && Char vx300 <= Char (Succ vx34) || Char vx300 >= Char (Succ vx35) && Char vx300 <= Char (Succ vx36)) || isLower (Char vx300)",fontsize=16,color="burlywood",shape="box"];2031[label="vx300/Succ vx3000",fontsize=10,color="white",style="solid",shape="box"];68 -> 2031[label="",style="solid", color="burlywood", weight=9];
2031 -> 69[label="",style="solid", color="burlywood", weight=3];
2032[label="vx300/Zero",fontsize=10,color="white",style="solid",shape="box"];68 -> 2032[label="",style="solid", color="burlywood", weight=9];
2032 -> 70[label="",style="solid", color="burlywood", weight=3];
69[label="(not (primCmpNat (Succ vx3000) (Succ vx31) == LT) && Char (Succ vx3000) <= Char (Succ vx32) || Char (Succ vx3000) >= Char (Succ vx33) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)) || isLower (Char (Succ vx3000))",fontsize=16,color="black",shape="box"];69 -> 71[label="",style="solid", color="black", weight=3];
70[label="(not (primCmpNat Zero (Succ vx31) == LT) && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];70 -> 72[label="",style="solid", color="black", weight=3];
71 -> 215[label="",style="dashed", color="red", weight=0];
71[label="(not (primCmpNat vx3000 vx31 == LT) && Char (Succ vx3000) <= Char (Succ vx32) || Char (Succ vx3000) >= Char (Succ vx33) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)) || isLower (Char (Succ vx3000))",fontsize=16,color="magenta"];71 -> 216[label="",style="dashed", color="magenta", weight=3];
71 -> 217[label="",style="dashed", color="magenta", weight=3];
71 -> 218[label="",style="dashed", color="magenta", weight=3];
71 -> 219[label="",style="dashed", color="magenta", weight=3];
71 -> 220[label="",style="dashed", color="magenta", weight=3];
71 -> 221[label="",style="dashed", color="magenta", weight=3];
71 -> 222[label="",style="dashed", color="magenta", weight=3];
71 -> 223[label="",style="dashed", color="magenta", weight=3];
72[label="(not (LT == LT) && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];72 -> 75[label="",style="solid", color="black", weight=3];
216[label="vx35",fontsize=16,color="green",shape="box"];217[label="vx31",fontsize=16,color="green",shape="box"];218[label="vx36",fontsize=16,color="green",shape="box"];219[label="vx3000",fontsize=16,color="green",shape="box"];220[label="vx34",fontsize=16,color="green",shape="box"];221[label="vx32",fontsize=16,color="green",shape="box"];222[label="vx3000",fontsize=16,color="green",shape="box"];223[label="vx33",fontsize=16,color="green",shape="box"];215[label="(not (primCmpNat vx38 vx39 == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="burlywood",shape="triangle"];2034[label="vx38/Succ vx380",fontsize=10,color="white",style="solid",shape="box"];215 -> 2034[label="",style="solid", color="burlywood", weight=9];
2034 -> 264[label="",style="solid", color="burlywood", weight=3];
2035[label="vx38/Zero",fontsize=10,color="white",style="solid",shape="box"];215 -> 2035[label="",style="solid", color="burlywood", weight=9];
2035 -> 265[label="",style="solid", color="burlywood", weight=3];
75[label="(not True && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];75 -> 80[label="",style="solid", color="black", weight=3];
264[label="(not (primCmpNat (Succ vx380) vx39 == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="burlywood",shape="box"];2036[label="vx39/Succ vx390",fontsize=10,color="white",style="solid",shape="box"];264 -> 2036[label="",style="solid", color="burlywood", weight=9];
2036 -> 267[label="",style="solid", color="burlywood", weight=3];
2037[label="vx39/Zero",fontsize=10,color="white",style="solid",shape="box"];264 -> 2037[label="",style="solid", color="burlywood", weight=9];
2037 -> 268[label="",style="solid", color="burlywood", weight=3];
265[label="(not (primCmpNat Zero vx39 == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="burlywood",shape="box"];2038[label="vx39/Succ vx390",fontsize=10,color="white",style="solid",shape="box"];265 -> 2038[label="",style="solid", color="burlywood", weight=9];
2038 -> 269[label="",style="solid", color="burlywood", weight=3];
2039[label="vx39/Zero",fontsize=10,color="white",style="solid",shape="box"];265 -> 2039[label="",style="solid", color="burlywood", weight=9];
2039 -> 270[label="",style="solid", color="burlywood", weight=3];
80[label="(False && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];80 -> 85[label="",style="solid", color="black", weight=3];
267[label="(not (primCmpNat (Succ vx380) (Succ vx390) == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];267 -> 272[label="",style="solid", color="black", weight=3];
268[label="(not (primCmpNat (Succ vx380) Zero == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];268 -> 273[label="",style="solid", color="black", weight=3];
269[label="(not (primCmpNat Zero (Succ vx390) == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];269 -> 274[label="",style="solid", color="black", weight=3];
270[label="(not (primCmpNat Zero Zero == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];270 -> 275[label="",style="solid", color="black", weight=3];
85[label="(False || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];85 -> 91[label="",style="solid", color="black", weight=3];
272 -> 215[label="",style="dashed", color="red", weight=0];
272[label="(not (primCmpNat vx380 vx390 == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="magenta"];272 -> 277[label="",style="dashed", color="magenta", weight=3];
272 -> 278[label="",style="dashed", color="magenta", weight=3];
273[label="(not (GT == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];273 -> 279[label="",style="solid", color="black", weight=3];
274[label="(not (LT == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];274 -> 280[label="",style="solid", color="black", weight=3];
275[label="(not (EQ == LT) && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];275 -> 281[label="",style="solid", color="black", weight=3];
91[label="(Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];91 -> 99[label="",style="solid", color="black", weight=3];
277[label="vx390",fontsize=16,color="green",shape="box"];278[label="vx380",fontsize=16,color="green",shape="box"];279[label="(not False && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="triangle"];279 -> 283[label="",style="solid", color="black", weight=3];
280[label="(not True && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];280 -> 284[label="",style="solid", color="black", weight=3];
281 -> 279[label="",style="dashed", color="red", weight=0];
281[label="(not False && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="magenta"];99[label="(compare (Char Zero) (Char (Succ vx33)) /= LT && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];99 -> 107[label="",style="solid", color="black", weight=3];
283[label="(True && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];283 -> 286[label="",style="solid", color="black", weight=3];
284[label="(False && Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];284 -> 287[label="",style="solid", color="black", weight=3];
107[label="(not (compare (Char Zero) (Char (Succ vx33)) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];107 -> 116[label="",style="solid", color="black", weight=3];
286[label="(Char (Succ vx40) <= Char (Succ vx41) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];286 -> 289[label="",style="solid", color="black", weight=3];
287[label="(False || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="triangle"];287 -> 290[label="",style="solid", color="black", weight=3];
116[label="(not (primCmpChar (Char Zero) (Char (Succ vx33)) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];116 -> 126[label="",style="solid", color="black", weight=3];
289[label="(compare (Char (Succ vx40)) (Char (Succ vx41)) /= GT || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];289 -> 292[label="",style="solid", color="black", weight=3];
290[label="(Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];290 -> 293[label="",style="solid", color="black", weight=3];
126[label="(not (primCmpNat Zero (Succ vx33) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];126 -> 135[label="",style="solid", color="black", weight=3];
292[label="(not (compare (Char (Succ vx40)) (Char (Succ vx41)) == GT) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];292 -> 295[label="",style="solid", color="black", weight=3];
293[label="(compare (Char (Succ vx40)) (Char (Succ vx42)) /= LT && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];293 -> 296[label="",style="solid", color="black", weight=3];
135[label="(not (LT == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];135 -> 145[label="",style="solid", color="black", weight=3];
295[label="(not (primCmpChar (Char (Succ vx40)) (Char (Succ vx41)) == GT) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];295 -> 299[label="",style="solid", color="black", weight=3];
296[label="(not (compare (Char (Succ vx40)) (Char (Succ vx42)) == LT) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];296 -> 300[label="",style="solid", color="black", weight=3];
145[label="(not True && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];145 -> 156[label="",style="solid", color="black", weight=3];
299 -> 548[label="",style="dashed", color="red", weight=0];
299[label="(not (primCmpNat (Succ vx40) (Succ vx41) == GT) || Char (Succ vx40) >= Char (Succ vx42) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="magenta"];299 -> 549[label="",style="dashed", color="magenta", weight=3];
299 -> 550[label="",style="dashed", color="magenta", weight=3];
299 -> 551[label="",style="dashed", color="magenta", weight=3];
299 -> 552[label="",style="dashed", color="magenta", weight=3];
299 -> 553[label="",style="dashed", color="magenta", weight=3];
299 -> 554[label="",style="dashed", color="magenta", weight=3];
299 -> 555[label="",style="dashed", color="magenta", weight=3];
300[label="(not (primCmpChar (Char (Succ vx40)) (Char (Succ vx42)) == LT) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="black",shape="box"];300 -> 307[label="",style="solid", color="black", weight=3];
156[label="(False && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];156 -> 168[label="",style="solid", color="black", weight=3];
549[label="vx45",fontsize=16,color="green",shape="box"];550[label="vx44",fontsize=16,color="green",shape="box"];551[label="vx43",fontsize=16,color="green",shape="box"];552[label="Succ vx40",fontsize=16,color="green",shape="box"];553[label="vx40",fontsize=16,color="green",shape="box"];554[label="vx42",fontsize=16,color="green",shape="box"];555[label="Succ vx41",fontsize=16,color="green",shape="box"];548[label="(not (primCmpNat vx74 vx75 == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="burlywood",shape="triangle"];2043[label="vx74/Succ vx740",fontsize=10,color="white",style="solid",shape="box"];548 -> 2043[label="",style="solid", color="burlywood", weight=9];
2043 -> 598[label="",style="solid", color="burlywood", weight=3];
2044[label="vx74/Zero",fontsize=10,color="white",style="solid",shape="box"];548 -> 2044[label="",style="solid", color="burlywood", weight=9];
2044 -> 599[label="",style="solid", color="burlywood", weight=3];
307 -> 620[label="",style="dashed", color="red", weight=0];
307[label="(not (primCmpNat (Succ vx40) (Succ vx42) == LT) && Char (Succ vx40) <= Char (Succ vx43) || Char (Succ vx40) >= Char (Succ vx44) && Char (Succ vx40) <= Char (Succ vx45)) || isLower (Char (Succ vx40))",fontsize=16,color="magenta"];307 -> 621[label="",style="dashed", color="magenta", weight=3];
307 -> 622[label="",style="dashed", color="magenta", weight=3];
307 -> 623[label="",style="dashed", color="magenta", weight=3];
307 -> 624[label="",style="dashed", color="magenta", weight=3];
307 -> 625[label="",style="dashed", color="magenta", weight=3];
307 -> 626[label="",style="dashed", color="magenta", weight=3];
168[label="(False || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];168 -> 182[label="",style="solid", color="black", weight=3];
598[label="(not (primCmpNat (Succ vx740) vx75 == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="burlywood",shape="box"];2046[label="vx75/Succ vx750",fontsize=10,color="white",style="solid",shape="box"];598 -> 2046[label="",style="solid", color="burlywood", weight=9];
2046 -> 616[label="",style="solid", color="burlywood", weight=3];
2047[label="vx75/Zero",fontsize=10,color="white",style="solid",shape="box"];598 -> 2047[label="",style="solid", color="burlywood", weight=9];
2047 -> 617[label="",style="solid", color="burlywood", weight=3];
599[label="(not (primCmpNat Zero vx75 == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="burlywood",shape="box"];2048[label="vx75/Succ vx750",fontsize=10,color="white",style="solid",shape="box"];599 -> 2048[label="",style="solid", color="burlywood", weight=9];
2048 -> 618[label="",style="solid", color="burlywood", weight=3];
2049[label="vx75/Zero",fontsize=10,color="white",style="solid",shape="box"];599 -> 2049[label="",style="solid", color="burlywood", weight=9];
2049 -> 619[label="",style="solid", color="burlywood", weight=3];
621[label="Succ vx42",fontsize=16,color="green",shape="box"];622[label="vx44",fontsize=16,color="green",shape="box"];623[label="vx45",fontsize=16,color="green",shape="box"];624[label="vx43",fontsize=16,color="green",shape="box"];625[label="vx40",fontsize=16,color="green",shape="box"];626[label="Succ vx40",fontsize=16,color="green",shape="box"];620[label="(not (primCmpNat vx82 vx83 == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="burlywood",shape="triangle"];2050[label="vx82/Succ vx820",fontsize=10,color="white",style="solid",shape="box"];620 -> 2050[label="",style="solid", color="burlywood", weight=9];
2050 -> 663[label="",style="solid", color="burlywood", weight=3];
2051[label="vx82/Zero",fontsize=10,color="white",style="solid",shape="box"];620 -> 2051[label="",style="solid", color="burlywood", weight=9];
2051 -> 664[label="",style="solid", color="burlywood", weight=3];
182[label="Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];182 -> 198[label="",style="solid", color="black", weight=3];
616[label="(not (primCmpNat (Succ vx740) (Succ vx750) == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];616 -> 665[label="",style="solid", color="black", weight=3];
617[label="(not (primCmpNat (Succ vx740) Zero == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];617 -> 666[label="",style="solid", color="black", weight=3];
618[label="(not (primCmpNat Zero (Succ vx750) == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];618 -> 667[label="",style="solid", color="black", weight=3];
619[label="(not (primCmpNat Zero Zero == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];619 -> 668[label="",style="solid", color="black", weight=3];
663[label="(not (primCmpNat (Succ vx820) vx83 == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="burlywood",shape="box"];2052[label="vx83/Succ vx830",fontsize=10,color="white",style="solid",shape="box"];663 -> 2052[label="",style="solid", color="burlywood", weight=9];
2052 -> 670[label="",style="solid", color="burlywood", weight=3];
2053[label="vx83/Zero",fontsize=10,color="white",style="solid",shape="box"];663 -> 2053[label="",style="solid", color="burlywood", weight=9];
2053 -> 671[label="",style="solid", color="burlywood", weight=3];
664[label="(not (primCmpNat Zero vx83 == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="burlywood",shape="box"];2054[label="vx83/Succ vx830",fontsize=10,color="white",style="solid",shape="box"];664 -> 2054[label="",style="solid", color="burlywood", weight=9];
2054 -> 672[label="",style="solid", color="burlywood", weight=3];
2055[label="vx83/Zero",fontsize=10,color="white",style="solid",shape="box"];664 -> 2055[label="",style="solid", color="burlywood", weight=9];
2055 -> 673[label="",style="solid", color="burlywood", weight=3];
198[label="compare (Char Zero) (Char (Succ vx35)) /= LT && Char Zero <= Char (Succ vx36) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];198 -> 214[label="",style="solid", color="black", weight=3];
665 -> 548[label="",style="dashed", color="red", weight=0];
665[label="(not (primCmpNat vx740 vx750 == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="magenta"];665 -> 674[label="",style="dashed", color="magenta", weight=3];
665 -> 675[label="",style="dashed", color="magenta", weight=3];
666[label="(not (GT == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];666 -> 676[label="",style="solid", color="black", weight=3];
667[label="(not (LT == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];667 -> 677[label="",style="solid", color="black", weight=3];
668[label="(not (EQ == GT) || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];668 -> 678[label="",style="solid", color="black", weight=3];
670[label="(not (primCmpNat (Succ vx820) (Succ vx830) == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];670 -> 680[label="",style="solid", color="black", weight=3];
671[label="(not (primCmpNat (Succ vx820) Zero == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];671 -> 681[label="",style="solid", color="black", weight=3];
672[label="(not (primCmpNat Zero (Succ vx830) == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];672 -> 682[label="",style="solid", color="black", weight=3];
673[label="(not (primCmpNat Zero Zero == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];673 -> 683[label="",style="solid", color="black", weight=3];
214[label="not (compare (Char Zero) (Char (Succ vx35)) == LT) && Char Zero <= Char (Succ vx36) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];214 -> 266[label="",style="solid", color="black", weight=3];
674[label="vx740",fontsize=16,color="green",shape="box"];675[label="vx750",fontsize=16,color="green",shape="box"];676[label="(not True || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];676 -> 684[label="",style="solid", color="black", weight=3];
677[label="(not False || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="triangle"];677 -> 685[label="",style="solid", color="black", weight=3];
678 -> 677[label="",style="dashed", color="red", weight=0];
678[label="(not False || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="magenta"];680 -> 620[label="",style="dashed", color="red", weight=0];
680[label="(not (primCmpNat vx820 vx830 == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="magenta"];680 -> 687[label="",style="dashed", color="magenta", weight=3];
680 -> 688[label="",style="dashed", color="magenta", weight=3];
681[label="(not (GT == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];681 -> 689[label="",style="solid", color="black", weight=3];
682[label="(not (LT == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];682 -> 690[label="",style="solid", color="black", weight=3];
683[label="(not (EQ == LT) && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];683 -> 691[label="",style="solid", color="black", weight=3];
266[label="not (primCmpChar (Char Zero) (Char (Succ vx35)) == LT) && Char Zero <= Char (Succ vx36) || isLower (Char Zero)",fontsize=16,color="black",shape="box"];266 -> 271[label="",style="solid", color="black", weight=3];
684 -> 287[label="",style="dashed", color="red", weight=0];
684[label="(False || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="magenta"];684 -> 692[label="",style="dashed", color="magenta", weight=3];
684 -> 693[label="",style="dashed", color="magenta", weight=3];
684 -> 694[label="",style="dashed", color="magenta", weight=3];
684 -> 695[label="",style="dashed", color="magenta", weight=3];
684 -> 696[label="",style="dashed", color="magenta", weight=3];
685[label="(True || Char (Succ vx76) >= Char (Succ vx77) && Char (Succ vx76) <= Char (Succ vx78) || Char (Succ vx76) >= Char (Succ vx79) && Char (Succ vx76) <= Char (Succ vx80)) || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="box"];685 -> 697[label="",style="solid", color="black", weight=3];
687[label="vx830",fontsize=16,color="green",shape="box"];688[label="vx820",fontsize=16,color="green",shape="box"];689[label="(not False && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="triangle"];689 -> 699[label="",style="solid", color="black", weight=3];
690[label="(not True && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];690 -> 700[label="",style="solid", color="black", weight=3];
691 -> 689[label="",style="dashed", color="red", weight=0];
691[label="(not False && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="magenta"];271 -> 1693[label="",style="dashed", color="red", weight=0];
271[label="not (primCmpNat Zero (Succ vx35) == LT) && Char Zero <= Char (Succ vx36) || isLower (Char Zero)",fontsize=16,color="magenta"];271 -> 1694[label="",style="dashed", color="magenta", weight=3];
271 -> 1695[label="",style="dashed", color="magenta", weight=3];
271 -> 1696[label="",style="dashed", color="magenta", weight=3];
271 -> 1697[label="",style="dashed", color="magenta", weight=3];
692[label="vx79",fontsize=16,color="green",shape="box"];693[label="vx80",fontsize=16,color="green",shape="box"];694[label="vx76",fontsize=16,color="green",shape="box"];695[label="vx78",fontsize=16,color="green",shape="box"];696[label="vx77",fontsize=16,color="green",shape="box"];697[label="True || isLower (Char (Succ vx76))",fontsize=16,color="black",shape="triangle"];697 -> 701[label="",style="solid", color="black", weight=3];
699[label="(True && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];699 -> 703[label="",style="solid", color="black", weight=3];
700[label="(False && Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];700 -> 704[label="",style="solid", color="black", weight=3];
1694[label="Succ vx35",fontsize=16,color="green",shape="box"];1695[label="Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="triangle"];1695 -> 1779[label="",style="solid", color="black", weight=3];
1696[label="Zero",fontsize=16,color="green",shape="box"];1697[label="isLower (Char Zero)",fontsize=16,color="black",shape="box"];1697 -> 1780[label="",style="solid", color="black", weight=3];
1693[label="not (primCmpNat vx1830000000 vx1860000000 == LT) && vx211 || vx204",fontsize=16,color="burlywood",shape="triangle"];2062[label="vx1830000000/Succ vx18300000000",fontsize=10,color="white",style="solid",shape="box"];1693 -> 2062[label="",style="solid", color="burlywood", weight=9];
2062 -> 1781[label="",style="solid", color="burlywood", weight=3];
2063[label="vx1830000000/Zero",fontsize=10,color="white",style="solid",shape="box"];1693 -> 2063[label="",style="solid", color="burlywood", weight=9];
2063 -> 1782[label="",style="solid", color="burlywood", weight=3];
701[label="True",fontsize=16,color="green",shape="box"];703[label="(Char (Succ vx84) <= Char (Succ vx85) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];703 -> 706[label="",style="solid", color="black", weight=3];
704[label="(False || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="triangle"];704 -> 707[label="",style="solid", color="black", weight=3];
1779[label="compare (Char Zero) (Char (Succ vx36)) /= GT",fontsize=16,color="black",shape="box"];1779 -> 1785[label="",style="solid", color="black", weight=3];
1780 -> 1838[label="",style="dashed", color="red", weight=0];
1780[label="Char Zero >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || Char Zero >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || Char Zero >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1780 -> 1839[label="",style="dashed", color="magenta", weight=3];
1780 -> 1840[label="",style="dashed", color="magenta", weight=3];
1780 -> 1841[label="",style="dashed", color="magenta", weight=3];
1780 -> 1842[label="",style="dashed", color="magenta", weight=3];
1780 -> 1843[label="",style="dashed", color="magenta", weight=3];
1780 -> 1844[label="",style="dashed", color="magenta", weight=3];
1781[label="not (primCmpNat (Succ vx18300000000) vx1860000000 == LT) && vx211 || vx204",fontsize=16,color="burlywood",shape="box"];2065[label="vx1860000000/Succ vx18600000000",fontsize=10,color="white",style="solid",shape="box"];1781 -> 2065[label="",style="solid", color="burlywood", weight=9];
2065 -> 1788[label="",style="solid", color="burlywood", weight=3];
2066[label="vx1860000000/Zero",fontsize=10,color="white",style="solid",shape="box"];1781 -> 2066[label="",style="solid", color="burlywood", weight=9];
2066 -> 1789[label="",style="solid", color="burlywood", weight=3];
1782[label="not (primCmpNat Zero vx1860000000 == LT) && vx211 || vx204",fontsize=16,color="burlywood",shape="box"];2067[label="vx1860000000/Succ vx18600000000",fontsize=10,color="white",style="solid",shape="box"];1782 -> 2067[label="",style="solid", color="burlywood", weight=9];
2067 -> 1790[label="",style="solid", color="burlywood", weight=3];
2068[label="vx1860000000/Zero",fontsize=10,color="white",style="solid",shape="box"];1782 -> 2068[label="",style="solid", color="burlywood", weight=9];
2068 -> 1791[label="",style="solid", color="burlywood", weight=3];
706[label="(compare (Char (Succ vx84)) (Char (Succ vx85)) /= GT || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];706 -> 709[label="",style="solid", color="black", weight=3];
707[label="Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];707 -> 710[label="",style="solid", color="black", weight=3];
1785[label="not (compare (Char Zero) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];1785 -> 1792[label="",style="solid", color="black", weight=3];
1839 -> 1695[label="",style="dashed", color="red", weight=0];
1839[label="Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1839 -> 1848[label="",style="dashed", color="magenta", weight=3];
1840[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1841[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1842 -> 1695[label="",style="dashed", color="red", weight=0];
1842[label="Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1842 -> 1849[label="",style="dashed", color="magenta", weight=3];
1843 -> 1695[label="",style="dashed", color="red", weight=0];
1843[label="Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1843 -> 1850[label="",style="dashed", color="magenta", weight=3];
1844[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1838[label="Char Zero >= Char (Succ vx233) && vx239 || Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="black",shape="triangle"];1838 -> 1851[label="",style="solid", color="black", weight=3];
1788[label="not (primCmpNat (Succ vx18300000000) (Succ vx18600000000) == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1788 -> 1852[label="",style="solid", color="black", weight=3];
1789[label="not (primCmpNat (Succ vx18300000000) Zero == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1789 -> 1853[label="",style="solid", color="black", weight=3];
1790[label="not (primCmpNat Zero (Succ vx18600000000) == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1790 -> 1854[label="",style="solid", color="black", weight=3];
1791[label="not (primCmpNat Zero Zero == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1791 -> 1855[label="",style="solid", color="black", weight=3];
709[label="(not (compare (Char (Succ vx84)) (Char (Succ vx85)) == GT) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];709 -> 712[label="",style="solid", color="black", weight=3];
710[label="compare (Char (Succ vx84)) (Char (Succ vx86)) /= LT && Char (Succ vx84) <= Char (Succ vx87) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];710 -> 713[label="",style="solid", color="black", weight=3];
1792[label="not (primCmpChar (Char Zero) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];1792 -> 1856[label="",style="solid", color="black", weight=3];
1848[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1849[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1850[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1851[label="compare (Char Zero) (Char (Succ vx233)) /= LT && vx239 || Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="black",shape="box"];1851 -> 1861[label="",style="solid", color="black", weight=3];
1852 -> 1693[label="",style="dashed", color="red", weight=0];
1852[label="not (primCmpNat vx18300000000 vx18600000000 == LT) && vx211 || vx204",fontsize=16,color="magenta"];1852 -> 1862[label="",style="dashed", color="magenta", weight=3];
1852 -> 1863[label="",style="dashed", color="magenta", weight=3];
1853[label="not (GT == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1853 -> 1864[label="",style="solid", color="black", weight=3];
1854[label="not (LT == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1854 -> 1865[label="",style="solid", color="black", weight=3];
1855[label="not (EQ == LT) && vx211 || vx204",fontsize=16,color="black",shape="box"];1855 -> 1866[label="",style="solid", color="black", weight=3];
712[label="(not (primCmpChar (Char (Succ vx84)) (Char (Succ vx85)) == GT) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];712 -> 715[label="",style="solid", color="black", weight=3];
713[label="not (compare (Char (Succ vx84)) (Char (Succ vx86)) == LT) && Char (Succ vx84) <= Char (Succ vx87) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];713 -> 716[label="",style="solid", color="black", weight=3];
1856[label="not (primCmpNat Zero (Succ vx36) == GT)",fontsize=16,color="black",shape="box"];1856 -> 1867[label="",style="solid", color="black", weight=3];
1861[label="not (compare (Char Zero) (Char (Succ vx233)) == LT) && vx239 || Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="black",shape="box"];1861 -> 1876[label="",style="solid", color="black", weight=3];
1862[label="vx18600000000",fontsize=16,color="green",shape="box"];1863[label="vx18300000000",fontsize=16,color="green",shape="box"];1864[label="not False && vx211 || vx204",fontsize=16,color="black",shape="triangle"];1864 -> 1877[label="",style="solid", color="black", weight=3];
1865[label="not True && vx211 || vx204",fontsize=16,color="black",shape="box"];1865 -> 1878[label="",style="solid", color="black", weight=3];
1866 -> 1864[label="",style="dashed", color="red", weight=0];
1866[label="not False && vx211 || vx204",fontsize=16,color="magenta"];715 -> 1001[label="",style="dashed", color="red", weight=0];
715[label="(not (primCmpNat (Succ vx84) (Succ vx85) == GT) || Char (Succ vx84) >= Char (Succ vx86) && Char (Succ vx84) <= Char (Succ vx87)) || isLower (Char (Succ vx84))",fontsize=16,color="magenta"];715 -> 1002[label="",style="dashed", color="magenta", weight=3];
715 -> 1003[label="",style="dashed", color="magenta", weight=3];
715 -> 1004[label="",style="dashed", color="magenta", weight=3];
715 -> 1005[label="",style="dashed", color="magenta", weight=3];
715 -> 1006[label="",style="dashed", color="magenta", weight=3];
716[label="not (primCmpChar (Char (Succ vx84)) (Char (Succ vx86)) == LT) && Char (Succ vx84) <= Char (Succ vx87) || isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];716 -> 719[label="",style="solid", color="black", weight=3];
1867[label="not (LT == GT)",fontsize=16,color="black",shape="triangle"];1867 -> 1879[label="",style="solid", color="black", weight=3];
1876[label="not (primCmpChar (Char Zero) (Char (Succ vx233)) == LT) && vx239 || Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="black",shape="box"];1876 -> 1889[label="",style="solid", color="black", weight=3];
1877[label="True && vx211 || vx204",fontsize=16,color="black",shape="box"];1877 -> 1890[label="",style="solid", color="black", weight=3];
1878[label="False && vx211 || vx204",fontsize=16,color="black",shape="box"];1878 -> 1891[label="",style="solid", color="black", weight=3];
1002[label="Succ vx85",fontsize=16,color="green",shape="box"];1003[label="Succ vx84",fontsize=16,color="green",shape="box"];1004[label="vx87",fontsize=16,color="green",shape="box"];1005[label="vx84",fontsize=16,color="green",shape="box"];1006[label="vx86",fontsize=16,color="green",shape="box"];1001[label="(not (primCmpNat vx144 vx145 == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="burlywood",shape="triangle"];2075[label="vx144/Succ vx1440",fontsize=10,color="white",style="solid",shape="box"];1001 -> 2075[label="",style="solid", color="burlywood", weight=9];
2075 -> 1037[label="",style="solid", color="burlywood", weight=3];
2076[label="vx144/Zero",fontsize=10,color="white",style="solid",shape="box"];1001 -> 2076[label="",style="solid", color="burlywood", weight=9];
2076 -> 1038[label="",style="solid", color="burlywood", weight=3];
719 -> 1693[label="",style="dashed", color="red", weight=0];
719[label="not (primCmpNat (Succ vx84) (Succ vx86) == LT) && Char (Succ vx84) <= Char (Succ vx87) || isLower (Char (Succ vx84))",fontsize=16,color="magenta"];719 -> 1698[label="",style="dashed", color="magenta", weight=3];
719 -> 1699[label="",style="dashed", color="magenta", weight=3];
719 -> 1700[label="",style="dashed", color="magenta", weight=3];
719 -> 1701[label="",style="dashed", color="magenta", weight=3];
1879[label="not False",fontsize=16,color="black",shape="triangle"];1879 -> 1892[label="",style="solid", color="black", weight=3];
1889 -> 1693[label="",style="dashed", color="red", weight=0];
1889[label="not (primCmpNat Zero (Succ vx233) == LT) && vx239 || Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="magenta"];1889 -> 1904[label="",style="dashed", color="magenta", weight=3];
1889 -> 1905[label="",style="dashed", color="magenta", weight=3];
1889 -> 1906[label="",style="dashed", color="magenta", weight=3];
1889 -> 1907[label="",style="dashed", color="magenta", weight=3];
1890[label="vx211 || vx204",fontsize=16,color="burlywood",shape="triangle"];2079[label="vx211/False",fontsize=10,color="white",style="solid",shape="box"];1890 -> 2079[label="",style="solid", color="burlywood", weight=9];
2079 -> 1908[label="",style="solid", color="burlywood", weight=3];
2080[label="vx211/True",fontsize=10,color="white",style="solid",shape="box"];1890 -> 2080[label="",style="solid", color="burlywood", weight=9];
2080 -> 1909[label="",style="solid", color="burlywood", weight=3];
1891 -> 1890[label="",style="dashed", color="red", weight=0];
1891[label="False || vx204",fontsize=16,color="magenta"];1891 -> 1910[label="",style="dashed", color="magenta", weight=3];
1037[label="(not (primCmpNat (Succ vx1440) vx145 == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="burlywood",shape="box"];2082[label="vx145/Succ vx1450",fontsize=10,color="white",style="solid",shape="box"];1037 -> 2082[label="",style="solid", color="burlywood", weight=9];
2082 -> 1046[label="",style="solid", color="burlywood", weight=3];
2083[label="vx145/Zero",fontsize=10,color="white",style="solid",shape="box"];1037 -> 2083[label="",style="solid", color="burlywood", weight=9];
2083 -> 1047[label="",style="solid", color="burlywood", weight=3];
1038[label="(not (primCmpNat Zero vx145 == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="burlywood",shape="box"];2084[label="vx145/Succ vx1450",fontsize=10,color="white",style="solid",shape="box"];1038 -> 2084[label="",style="solid", color="burlywood", weight=9];
2084 -> 1048[label="",style="solid", color="burlywood", weight=3];
2085[label="vx145/Zero",fontsize=10,color="white",style="solid",shape="box"];1038 -> 2085[label="",style="solid", color="burlywood", weight=9];
2085 -> 1049[label="",style="solid", color="burlywood", weight=3];
1698[label="Succ vx86",fontsize=16,color="green",shape="box"];1699[label="Char (Succ vx84) <= Char (Succ vx87)",fontsize=16,color="black",shape="triangle"];1699 -> 1783[label="",style="solid", color="black", weight=3];
1700[label="Succ vx84",fontsize=16,color="green",shape="box"];1701[label="isLower (Char (Succ vx84))",fontsize=16,color="black",shape="box"];1701 -> 1784[label="",style="solid", color="black", weight=3];
1892[label="True",fontsize=16,color="green",shape="box"];1904[label="Succ vx233",fontsize=16,color="green",shape="box"];1905[label="vx239",fontsize=16,color="green",shape="box"];1906[label="Zero",fontsize=16,color="green",shape="box"];1907 -> 1890[label="",style="dashed", color="red", weight=0];
1907[label="Char Zero >= Char (Succ vx235) && vx241 || Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="magenta"];1907 -> 1914[label="",style="dashed", color="magenta", weight=3];
1907 -> 1915[label="",style="dashed", color="magenta", weight=3];
1908[label="False || vx204",fontsize=16,color="black",shape="box"];1908 -> 1916[label="",style="solid", color="black", weight=3];
1909[label="True || vx204",fontsize=16,color="black",shape="box"];1909 -> 1917[label="",style="solid", color="black", weight=3];
1910[label="False",fontsize=16,color="green",shape="box"];1046[label="(not (primCmpNat (Succ vx1440) (Succ vx1450) == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1046 -> 1091[label="",style="solid", color="black", weight=3];
1047[label="(not (primCmpNat (Succ vx1440) Zero == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1047 -> 1092[label="",style="solid", color="black", weight=3];
1048[label="(not (primCmpNat Zero (Succ vx1450) == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1048 -> 1093[label="",style="solid", color="black", weight=3];
1049[label="(not (primCmpNat Zero Zero == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1049 -> 1094[label="",style="solid", color="black", weight=3];
1783[label="compare (Char (Succ vx84)) (Char (Succ vx87)) /= GT",fontsize=16,color="black",shape="box"];1783 -> 1857[label="",style="solid", color="black", weight=3];
1784 -> 1893[label="",style="dashed", color="red", weight=0];
1784[label="Char (Succ vx84) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx84) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || Char (Succ vx84) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx84) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || Char (Succ vx84) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx84) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1784 -> 1894[label="",style="dashed", color="magenta", weight=3];
1784 -> 1895[label="",style="dashed", color="magenta", weight=3];
1784 -> 1896[label="",style="dashed", color="magenta", weight=3];
1784 -> 1897[label="",style="dashed", color="magenta", weight=3];
1784 -> 1898[label="",style="dashed", color="magenta", weight=3];
1914 -> 1963[label="",style="dashed", color="red", weight=0];
1914[label="Char Zero >= Char (Succ vx235) && vx241",fontsize=16,color="magenta"];1914 -> 1964[label="",style="dashed", color="magenta", weight=3];
1915 -> 1963[label="",style="dashed", color="red", weight=0];
1915[label="Char Zero >= Char (Succ vx237) && vx240",fontsize=16,color="magenta"];1915 -> 1965[label="",style="dashed", color="magenta", weight=3];
1915 -> 1966[label="",style="dashed", color="magenta", weight=3];
1916[label="vx204",fontsize=16,color="green",shape="box"];1917[label="True",fontsize=16,color="green",shape="box"];1091 -> 1001[label="",style="dashed", color="red", weight=0];
1091[label="(not (primCmpNat vx1440 vx1450 == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="magenta"];1091 -> 1099[label="",style="dashed", color="magenta", weight=3];
1091 -> 1100[label="",style="dashed", color="magenta", weight=3];
1092[label="(not (GT == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1092 -> 1101[label="",style="solid", color="black", weight=3];
1093[label="(not (LT == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1093 -> 1102[label="",style="solid", color="black", weight=3];
1094[label="(not (EQ == GT) || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1094 -> 1103[label="",style="solid", color="black", weight=3];
1857[label="not (compare (Char (Succ vx84)) (Char (Succ vx87)) == GT)",fontsize=16,color="black",shape="box"];1857 -> 1868[label="",style="solid", color="black", weight=3];
1894[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1895[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1896[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1897[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1898[label="vx84",fontsize=16,color="green",shape="box"];1893 -> 1890[label="",style="dashed", color="red", weight=0];
1893[label="Char (Succ vx255) >= Char (Succ vx256) && Char (Succ vx255) <= Char (Succ vx257) || Char (Succ vx255) >= Char (Succ vx258) && Char (Succ vx255) <= Char (Succ vx259) || Char (Succ vx255) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx255) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1893 -> 1911[label="",style="dashed", color="magenta", weight=3];
1893 -> 1912[label="",style="dashed", color="magenta", weight=3];
1964[label="Char Zero >= Char (Succ vx235)",fontsize=16,color="black",shape="triangle"];1964 -> 1991[label="",style="solid", color="black", weight=3];
1963[label="vx261 && vx241",fontsize=16,color="burlywood",shape="triangle"];2092[label="vx261/False",fontsize=10,color="white",style="solid",shape="box"];1963 -> 2092[label="",style="solid", color="burlywood", weight=9];
2092 -> 1992[label="",style="solid", color="burlywood", weight=3];
2093[label="vx261/True",fontsize=10,color="white",style="solid",shape="box"];1963 -> 2093[label="",style="solid", color="burlywood", weight=9];
2093 -> 1993[label="",style="solid", color="burlywood", weight=3];
1965 -> 1964[label="",style="dashed", color="red", weight=0];
1965[label="Char Zero >= Char (Succ vx237)",fontsize=16,color="magenta"];1965 -> 1994[label="",style="dashed", color="magenta", weight=3];
1966[label="vx240",fontsize=16,color="green",shape="box"];1099[label="vx1450",fontsize=16,color="green",shape="box"];1100[label="vx1440",fontsize=16,color="green",shape="box"];1101[label="(not True || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1101 -> 1108[label="",style="solid", color="black", weight=3];
1102[label="(not False || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="triangle"];1102 -> 1109[label="",style="solid", color="black", weight=3];
1103 -> 1102[label="",style="dashed", color="red", weight=0];
1103[label="(not False || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="magenta"];1868[label="not (primCmpChar (Char (Succ vx84)) (Char (Succ vx87)) == GT)",fontsize=16,color="black",shape="box"];1868 -> 1913[label="",style="solid", color="black", weight=3];
1911 -> 1963[label="",style="dashed", color="red", weight=0];
1911[label="Char (Succ vx255) >= Char (Succ vx256) && Char (Succ vx255) <= Char (Succ vx257)",fontsize=16,color="magenta"];1911 -> 1968[label="",style="dashed", color="magenta", weight=3];
1911 -> 1969[label="",style="dashed", color="magenta", weight=3];
1912 -> 1890[label="",style="dashed", color="red", weight=0];
1912[label="Char (Succ vx255) >= Char (Succ vx258) && Char (Succ vx255) <= Char (Succ vx259) || Char (Succ vx255) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx255) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1912 -> 1923[label="",style="dashed", color="magenta", weight=3];
1912 -> 1924[label="",style="dashed", color="magenta", weight=3];
1991[label="compare (Char Zero) (Char (Succ vx235)) /= LT",fontsize=16,color="black",shape="box"];1991 -> 2004[label="",style="solid", color="black", weight=3];
1992[label="False && vx241",fontsize=16,color="black",shape="box"];1992 -> 2005[label="",style="solid", color="black", weight=3];
1993[label="True && vx241",fontsize=16,color="black",shape="box"];1993 -> 2006[label="",style="solid", color="black", weight=3];
1994[label="vx237",fontsize=16,color="green",shape="box"];1108 -> 704[label="",style="dashed", color="red", weight=0];
1108[label="(False || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="magenta"];1108 -> 1115[label="",style="dashed", color="magenta", weight=3];
1108 -> 1116[label="",style="dashed", color="magenta", weight=3];
1108 -> 1117[label="",style="dashed", color="magenta", weight=3];
1109[label="(True || Char (Succ vx146) >= Char (Succ vx147) && Char (Succ vx146) <= Char (Succ vx148)) || isLower (Char (Succ vx146))",fontsize=16,color="black",shape="box"];1109 -> 1118[label="",style="solid", color="black", weight=3];
1913[label="not (primCmpNat (Succ vx84) (Succ vx87) == GT)",fontsize=16,color="black",shape="box"];1913 -> 1925[label="",style="solid", color="black", weight=3];
1968[label="Char (Succ vx255) >= Char (Succ vx256)",fontsize=16,color="black",shape="triangle"];1968 -> 1995[label="",style="solid", color="black", weight=3];
1969 -> 1699[label="",style="dashed", color="red", weight=0];
1969[label="Char (Succ vx255) <= Char (Succ vx257)",fontsize=16,color="magenta"];1969 -> 1996[label="",style="dashed", color="magenta", weight=3];
1969 -> 1997[label="",style="dashed", color="magenta", weight=3];
1923 -> 1963[label="",style="dashed", color="red", weight=0];
1923[label="Char (Succ vx255) >= Char (Succ vx258) && Char (Succ vx255) <= Char (Succ vx259)",fontsize=16,color="magenta"];1923 -> 1973[label="",style="dashed", color="magenta", weight=3];
1923 -> 1974[label="",style="dashed", color="magenta", weight=3];
1924 -> 1963[label="",style="dashed", color="red", weight=0];
1924[label="Char (Succ vx255) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx255) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1924 -> 1975[label="",style="dashed", color="magenta", weight=3];
1924 -> 1976[label="",style="dashed", color="magenta", weight=3];
2004[label="not (compare (Char Zero) (Char (Succ vx235)) == LT)",fontsize=16,color="black",shape="box"];2004 -> 2008[label="",style="solid", color="black", weight=3];
2005[label="False",fontsize=16,color="green",shape="box"];2006[label="vx241",fontsize=16,color="green",shape="box"];1115[label="vx147",fontsize=16,color="green",shape="box"];1116[label="vx148",fontsize=16,color="green",shape="box"];1117[label="vx146",fontsize=16,color="green",shape="box"];1118 -> 697[label="",style="dashed", color="red", weight=0];
1118[label="True || isLower (Char (Succ vx146))",fontsize=16,color="magenta"];1118 -> 1121[label="",style="dashed", color="magenta", weight=3];
1925[label="not (primCmpNat vx84 vx87 == GT)",fontsize=16,color="burlywood",shape="triangle"];2103[label="vx84/Succ vx840",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2103[label="",style="solid", color="burlywood", weight=9];
2103 -> 1934[label="",style="solid", color="burlywood", weight=3];
2104[label="vx84/Zero",fontsize=10,color="white",style="solid",shape="box"];1925 -> 2104[label="",style="solid", color="burlywood", weight=9];
2104 -> 1935[label="",style="solid", color="burlywood", weight=3];
1995[label="compare (Char (Succ vx255)) (Char (Succ vx256)) /= LT",fontsize=16,color="black",shape="box"];1995 -> 2007[label="",style="solid", color="black", weight=3];
1996[label="vx257",fontsize=16,color="green",shape="box"];1997[label="vx255",fontsize=16,color="green",shape="box"];1973 -> 1968[label="",style="dashed", color="red", weight=0];
1973[label="Char (Succ vx255) >= Char (Succ vx258)",fontsize=16,color="magenta"];1973 -> 1998[label="",style="dashed", color="magenta", weight=3];
1974 -> 1699[label="",style="dashed", color="red", weight=0];
1974[label="Char (Succ vx255) <= Char (Succ vx259)",fontsize=16,color="magenta"];1974 -> 1999[label="",style="dashed", color="magenta", weight=3];
1974 -> 2000[label="",style="dashed", color="magenta", weight=3];
1975 -> 1968[label="",style="dashed", color="red", weight=0];
1975[label="Char (Succ vx255) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1975 -> 2001[label="",style="dashed", color="magenta", weight=3];
1976 -> 1699[label="",style="dashed", color="red", weight=0];
1976[label="Char (Succ vx255) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1976 -> 2002[label="",style="dashed", color="magenta", weight=3];
1976 -> 2003[label="",style="dashed", color="magenta", weight=3];
2008[label="not (primCmpChar (Char Zero) (Char (Succ vx235)) == LT)",fontsize=16,color="black",shape="box"];2008 -> 2010[label="",style="solid", color="black", weight=3];
1121[label="vx146",fontsize=16,color="green",shape="box"];1934[label="not (primCmpNat (Succ vx840) vx87 == GT)",fontsize=16,color="burlywood",shape="box"];2109[label="vx87/Succ vx870",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2109[label="",style="solid", color="burlywood", weight=9];
2109 -> 1942[label="",style="solid", color="burlywood", weight=3];
2110[label="vx87/Zero",fontsize=10,color="white",style="solid",shape="box"];1934 -> 2110[label="",style="solid", color="burlywood", weight=9];
2110 -> 1943[label="",style="solid", color="burlywood", weight=3];
1935[label="not (primCmpNat Zero vx87 == GT)",fontsize=16,color="burlywood",shape="box"];2111[label="vx87/Succ vx870",fontsize=10,color="white",style="solid",shape="box"];1935 -> 2111[label="",style="solid", color="burlywood", weight=9];
2111 -> 1944[label="",style="solid", color="burlywood", weight=3];
2112[label="vx87/Zero",fontsize=10,color="white",style="solid",shape="box"];1935 -> 2112[label="",style="solid", color="burlywood", weight=9];
2112 -> 1945[label="",style="solid", color="burlywood", weight=3];
2007[label="not (compare (Char (Succ vx255)) (Char (Succ vx256)) == LT)",fontsize=16,color="black",shape="box"];2007 -> 2009[label="",style="solid", color="black", weight=3];
1998[label="vx258",fontsize=16,color="green",shape="box"];1999[label="vx259",fontsize=16,color="green",shape="box"];2000[label="vx255",fontsize=16,color="green",shape="box"];2001[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];2002[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];2003[label="vx255",fontsize=16,color="green",shape="box"];2010[label="not (primCmpNat Zero (Succ vx235) == LT)",fontsize=16,color="black",shape="box"];2010 -> 2012[label="",style="solid", color="black", weight=3];
1942[label="not (primCmpNat (Succ vx840) (Succ vx870) == GT)",fontsize=16,color="black",shape="box"];1942 -> 1948[label="",style="solid", color="black", weight=3];
1943[label="not (primCmpNat (Succ vx840) Zero == GT)",fontsize=16,color="black",shape="box"];1943 -> 1949[label="",style="solid", color="black", weight=3];
1944[label="not (primCmpNat Zero (Succ vx870) == GT)",fontsize=16,color="black",shape="box"];1944 -> 1950[label="",style="solid", color="black", weight=3];
1945[label="not (primCmpNat Zero Zero == GT)",fontsize=16,color="black",shape="box"];1945 -> 1951[label="",style="solid", color="black", weight=3];
2009[label="not (primCmpChar (Char (Succ vx255)) (Char (Succ vx256)) == LT)",fontsize=16,color="black",shape="box"];2009 -> 2011[label="",style="solid", color="black", weight=3];
2012[label="not (LT == LT)",fontsize=16,color="black",shape="triangle"];2012 -> 2014[label="",style="solid", color="black", weight=3];
1948 -> 1925[label="",style="dashed", color="red", weight=0];
1948[label="not (primCmpNat vx840 vx870 == GT)",fontsize=16,color="magenta"];1948 -> 1954[label="",style="dashed", color="magenta", weight=3];
1948 -> 1955[label="",style="dashed", color="magenta", weight=3];
1949[label="not (GT == GT)",fontsize=16,color="black",shape="box"];1949 -> 1956[label="",style="solid", color="black", weight=3];
1950 -> 1867[label="",style="dashed", color="red", weight=0];
1950[label="not (LT == GT)",fontsize=16,color="magenta"];1951[label="not (EQ == GT)",fontsize=16,color="black",shape="box"];1951 -> 1957[label="",style="solid", color="black", weight=3];
2011[label="not (primCmpNat (Succ vx255) (Succ vx256) == LT)",fontsize=16,color="black",shape="box"];2011 -> 2013[label="",style="solid", color="black", weight=3];
2014 -> 1956[label="",style="dashed", color="red", weight=0];
2014[label="not True",fontsize=16,color="magenta"];1954[label="vx870",fontsize=16,color="green",shape="box"];1955[label="vx840",fontsize=16,color="green",shape="box"];1956[label="not True",fontsize=16,color="black",shape="triangle"];1956 -> 1960[label="",style="solid", color="black", weight=3];
1957 -> 1879[label="",style="dashed", color="red", weight=0];
1957[label="not False",fontsize=16,color="magenta"];2013[label="not (primCmpNat vx255 vx256 == LT)",fontsize=16,color="burlywood",shape="triangle"];2117[label="vx255/Succ vx2550",fontsize=10,color="white",style="solid",shape="box"];2013 -> 2117[label="",style="solid", color="burlywood", weight=9];
2117 -> 2015[label="",style="solid", color="burlywood", weight=3];
2118[label="vx255/Zero",fontsize=10,color="white",style="solid",shape="box"];2013 -> 2118[label="",style="solid", color="burlywood", weight=9];
2118 -> 2016[label="",style="solid", color="burlywood", weight=3];
1960[label="False",fontsize=16,color="green",shape="box"];2015[label="not (primCmpNat (Succ vx2550) vx256 == LT)",fontsize=16,color="burlywood",shape="box"];2119[label="vx256/Succ vx2560",fontsize=10,color="white",style="solid",shape="box"];2015 -> 2119[label="",style="solid", color="burlywood", weight=9];
2119 -> 2017[label="",style="solid", color="burlywood", weight=3];
2120[label="vx256/Zero",fontsize=10,color="white",style="solid",shape="box"];2015 -> 2120[label="",style="solid", color="burlywood", weight=9];
2120 -> 2018[label="",style="solid", color="burlywood", weight=3];
2016[label="not (primCmpNat Zero vx256 == LT)",fontsize=16,color="burlywood",shape="box"];2121[label="vx256/Succ vx2560",fontsize=10,color="white",style="solid",shape="box"];2016 -> 2121[label="",style="solid", color="burlywood", weight=9];
2121 -> 2019[label="",style="solid", color="burlywood", weight=3];
2122[label="vx256/Zero",fontsize=10,color="white",style="solid",shape="box"];2016 -> 2122[label="",style="solid", color="burlywood", weight=9];
2122 -> 2020[label="",style="solid", color="burlywood", weight=3];
2017[label="not (primCmpNat (Succ vx2550) (Succ vx2560) == LT)",fontsize=16,color="black",shape="box"];2017 -> 2021[label="",style="solid", color="black", weight=3];
2018[label="not (primCmpNat (Succ vx2550) Zero == LT)",fontsize=16,color="black",shape="box"];2018 -> 2022[label="",style="solid", color="black", weight=3];
2019[label="not (primCmpNat Zero (Succ vx2560) == LT)",fontsize=16,color="black",shape="box"];2019 -> 2023[label="",style="solid", color="black", weight=3];
2020[label="not (primCmpNat Zero Zero == LT)",fontsize=16,color="black",shape="box"];2020 -> 2024[label="",style="solid", color="black", weight=3];
2021 -> 2013[label="",style="dashed", color="red", weight=0];
2021[label="not (primCmpNat vx2550 vx2560 == LT)",fontsize=16,color="magenta"];2021 -> 2025[label="",style="dashed", color="magenta", weight=3];
2021 -> 2026[label="",style="dashed", color="magenta", weight=3];
2022[label="not (GT == LT)",fontsize=16,color="black",shape="box"];2022 -> 2027[label="",style="solid", color="black", weight=3];
2023 -> 2012[label="",style="dashed", color="red", weight=0];
2023[label="not (LT == LT)",fontsize=16,color="magenta"];2024[label="not (EQ == LT)",fontsize=16,color="black",shape="box"];2024 -> 2028[label="",style="solid", color="black", weight=3];
2025[label="vx2560",fontsize=16,color="green",shape="box"];2026[label="vx2550",fontsize=16,color="green",shape="box"];2027 -> 1879[label="",style="dashed", color="red", weight=0];
2027[label="not False",fontsize=16,color="magenta"];2028 -> 1879[label="",style="dashed", color="red", weight=0];
2028[label="not False",fontsize=16,color="magenta"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx2550), Succ(vx2560)) → new_not(vx2550, vx2560)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_not(Succ(vx2550), Succ(vx2560)) → new_not(vx2550, vx2560)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not0(Succ(vx840), Succ(vx870)) → new_not0(vx840, vx870)

From the DPs we obtained the following set of size-change graphs:

new_not0(Succ(vx840), Succ(vx870)) → new_not0(vx840, vx870)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_pePe(Succ(vx18300000000), Succ(vx18600000000), vx211, vx204) → new_pePe(vx18300000000, vx18600000000, vx211, vx204)

From the DPs we obtained the following set of size-change graphs:

new_pePe(Succ(vx18300000000), Succ(vx18600000000), vx211, vx204) → new_pePe(vx18300000000, vx18600000000, vx211, vx204)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_pePe0(Succ(vx1440), Succ(vx1450), vx146, vx147, vx148) → new_pePe0(vx1440, vx1450, vx146, vx147, vx148)

From the DPs we obtained the following set of size-change graphs:

new_pePe0(Succ(vx1440), Succ(vx1450), vx146, vx147, vx148) → new_pePe0(vx1440, vx1450, vx146, vx147, vx148)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_pePe1(Succ(vx820), Succ(vx830), vx84, vx85, vx86, vx87) → new_pePe1(vx820, vx830, vx84, vx85, vx86, vx87)

From the DPs we obtained the following set of size-change graphs:

new_pePe1(Succ(vx820), Succ(vx830), vx84, vx85, vx86, vx87) → new_pePe1(vx820, vx830, vx84, vx85, vx86, vx87)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_pePe2(Succ(vx740), Succ(vx750), vx76, vx77, vx78, vx79, vx80) → new_pePe2(vx740, vx750, vx76, vx77, vx78, vx79, vx80)

From the DPs we obtained the following set of size-change graphs:

new_pePe2(Succ(vx740), Succ(vx750), vx76, vx77, vx78, vx79, vx80) → new_pePe2(vx740, vx750, vx76, vx77, vx78, vx79, vx80)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_pePe3(Succ(vx380), Succ(vx390), vx40, vx41, vx42, vx43, vx44, vx45) → new_pePe3(vx380, vx390, vx40, vx41, vx42, vx43, vx44, vx45)

From the DPs we obtained the following set of size-change graphs:

new_pePe3(Succ(vx380), Succ(vx390), vx40, vx41, vx42, vx43, vx44, vx45) → new_pePe3(vx380, vx390, vx40, vx41, vx42, vx43, vx44, vx45)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8